\section{Conclusion}

To our knowledge, little help is provided  by compilers to ensure properties
such as completeness or disjointness. Consequently, the programmer is
responsible for ensuring them when they are needed. This task can quickly become
frustrating as the complexity of the pattern matching expression grows.
Moreover, it is natural to expect the compiler to ensure such properties, as it
is possible in many situations to statically determine whether they hold or
not.

We have shown that formal verification techniques can be used to improve the
current situation. Even though we haven't shown our approach to be sound, we
believe we have laid the groundwork for extending the Scala compiler with a
plugin which would allow developers to automatically check the completeness or
disjointness of their pattern matching expressions. 
